#!/bin/bash
# ulimit -v 4194304  # Set the virtual memory limit to 2GB
ulimit -v 8388608  # Set the virtual memory limit to 2GB

bench_dir=$2
exec_bin=$3
executeCase() {
    local ltlf_file=$1
    local tlsf_file="${ltlf_file%.ltlf}.tlsf"
    local part_file="${ltlf_file%.ltlf}.var"
    if [ ! -e "$part_file" ]; then
        part_file="${ltlf_file%.ltlf}.part"
    fi
    local res_file="${ltlf_file%.ltlf}.res"
    local pbs_file="${ltlf_file%.ltlf}.pbs"
    local pbs_id="${ltlf_file%.ltlf}"

    set -x

    ltlf_file=$bench_dir/$ltlf_file
    tlsf_file=$bench_dir/$tlsf_file
    part_file=$bench_dir/$part_file
    res_file=$bench_dir/$res_file

    cd /public/home/jwli/workSpace/yongkang/qsub_trash
    exec_base=$(basename $exec_bin)

    # timeout_mins=5
    # timeout_mins=10
    timeout_mins=30
    timeout_secs=$((timeout_mins * 60 + 30))

    if [[ $exec_base == XXXX* ]]; then
        echo 'ERROR: just EMPTY placeholder' > $res_file
    elif [[ $exec_base == ltlfsyn_sys_COMBINE01-splitAnd-sort* ]]; then
        export METHOD2_FLAG=0
        export SPLIT_AND=1
        # ltlfsyn sys_combine01-splitAnd
        export TIME_LIMIT=$timeout_mins
        export SAT_TRACE=1
        export SORT_FLAG=1
        (/usr/bin/time -v timeout $timeout_secs $exec_bin $ltlf_file $part_file) &> $res_file
    elif [[ $exec_base == ltlfsyn_sys_COMBINE01-splitAnd* ]]; then
        export METHOD2_FLAG=0
        export SPLIT_AND=1
        # ltlfsyn sys_combine01-splitAnd
        export TIME_LIMIT=$timeout_mins
        export SAT_TRACE=1
        (/usr/bin/time -v timeout $timeout_secs $exec_bin $ltlf_file $part_file) &> $res_file
    elif [[ $exec_base == ltlfsyn_sys_COMBINE01-sort* ]]; then
        export METHOD2_FLAG=0
        # ltlfsyn sys_combine01-splitAnd
        export TIME_LIMIT=$timeout_mins
        export SAT_TRACE=1
        export SORT_FLAG=1
        (/usr/bin/time -v timeout $timeout_secs $exec_bin $ltlf_file $part_file) &> $res_file
    elif [[ $exec_base == ltlfsyn_sys_COMBINE01* ]]; then
        export METHOD2_FLAG=0
        # ltlfsyn sys_combine01-raw
        export TIME_LIMIT=$timeout_mins
        export SAT_TRACE=1
        (/usr/bin/time -v timeout $timeout_secs $exec_bin $ltlf_file $part_file) &> $res_file
    elif [[ $exec_base == ltlfsyn_sys_COMBINE02-sysGroup-sort-level* ]]; then
        local level=$(echo "$exec_base" | grep -oP 'level\K[0-9]+')
        export METHOD2_FLAG=1
        export SYS_GROUP=1
        export SYS_GROUP_LEVEL=$level
        export SPLIT_AND=1
        export SORT_FLAG=1
        # ltlfsyn sys_combine02-splitAnd
        export TIME_LIMIT=$timeout_mins
        export SAT_TRACE=1
        (/usr/bin/time -v timeout $timeout_secs $exec_bin $ltlf_file $part_file) &> $res_file
    elif [[ $exec_base == ltlfsyn_sys_COMBINE02-sysGroup-level* ]]; then
        local level=$(echo "$exec_base" | grep -oP 'level\K[0-9]+')
        export METHOD2_FLAG=1
        export SYS_GROUP=1
        export SYS_GROUP_LEVEL=$level
        export SPLIT_AND=1
        # ltlfsyn sys_combine02-splitAnd
        export TIME_LIMIT=$timeout_mins
        export SAT_TRACE=1
        (/usr/bin/time -v timeout $timeout_secs $exec_bin $ltlf_file $part_file) &> $res_file
    elif [[ $exec_base == ltlfsyn_sys_COMBINE02-sysGroup-sort* ]]; then
        export METHOD2_FLAG=1
        export SPLIT_AND=1
        export SYS_GROUP=1
        export SORT_FLAG=1
        # ltlfsyn sys_combine02-splitAnd
        export TIME_LIMIT=$timeout_mins
        export SAT_TRACE=1
        (/usr/bin/time -v timeout $timeout_secs $exec_bin $ltlf_file $part_file) &> $res_file
    elif [[ $exec_base == ltlfsyn_sys_COMBINE02-sysGroup* ]]; then
        export METHOD2_FLAG=1
        export SPLIT_AND=1
        export SYS_GROUP=1
        # ltlfsyn sys_combine02-splitAnd
        export TIME_LIMIT=$timeout_mins
        export SAT_TRACE=1
        (/usr/bin/time -v timeout $timeout_secs $exec_bin $ltlf_file $part_file) &> $res_file
    elif [[ $exec_base == ltlfsyn_sys_COMBINE02-splitAnd-sort* ]]; then
        export METHOD2_FLAG=1
        export SPLIT_AND=1
        export SORT_FLAG=1
        # ltlfsyn sys_combine02-splitAnd
        export TIME_LIMIT=$timeout_mins
        export SAT_TRACE=1
        (/usr/bin/time -v timeout $timeout_secs $exec_bin $ltlf_file $part_file) &> $res_file
    elif [[ $exec_base == ltlfsyn_sys_COMBINE02-splitAnd* ]]; then
        export METHOD2_FLAG=1
        export SPLIT_AND=1
        # ltlfsyn sys_combine02-splitAnd
        export TIME_LIMIT=$timeout_mins
        export SAT_TRACE=1
        (/usr/bin/time -v timeout $timeout_secs $exec_bin $ltlf_file $part_file) &> $res_file
    elif [[ $exec_base == ltlfsyn_sys_COMBINE02-sort* ]]; then
        export METHOD2_FLAG=1
        export SORT_FLAG=1
        # ltlfsyn sys_combine02-raw
        export TIME_LIMIT=$timeout_mins
        export SAT_TRACE=1
        (/usr/bin/time -v timeout $timeout_secs $exec_bin $ltlf_file $part_file) &> $res_file
    elif [[ $exec_base == ltlfsyn_sys_COMBINE02* ]]; then
        export METHOD2_FLAG=1
        # ltlfsyn sys_combine02-raw
        export TIME_LIMIT=$timeout_mins
        export SAT_TRACE=1
        (/usr/bin/time -v timeout $timeout_secs $exec_bin $ltlf_file $part_file) &> $res_file
    elif [[ $exec_base == ltlfsyn_sys_SATtrace* ]]; then
        # ltlfsyn sys_SATtrace
        export TIME_LIMIT=$timeout_mins
        export SAT_TRACE=1
        (/usr/bin/time -v timeout $timeout_secs $exec_bin $ltlf_file $part_file) &> $res_file
    elif [[ $exec_base == ltlfsyn_sys_OneStep* ]]; then
        # ltlfsyn sys_OneStep
        export TIME_LIMIT=$timeout_mins
        export SAT_TRACE=0
        (/usr/bin/time -v timeout $timeout_secs $exec_bin $ltlf_file $part_file) &> $res_file
    elif [[ $exec_base == ltlfsyn_env_SATtrace* ]]; then
        # ltlfsyn env_SATtrace
        export TIME_LIMIT=$timeout_mins
        export SAT_TRACE=1
        (time timeout $timeout_secs $exec_bin $ltlf_file $part_file) &> $res_file
    elif [[ $exec_base == ltlfsyn_env_OneStep* ]]; then
        # ltlfsyn env_OneStep
        export TIME_LIMIT=$timeout_mins
        export SAT_TRACE=0
        (/usr/bin/time -v timeout $timeout_secs $exec_bin $ltlf_file $part_file) &> $res_file
    elif [[ $exec_base == ltlfsyn_sys* ]]; then
        # ltlfsyn sys
        export TIME_LIMIT=$timeout_mins
        export WHICH_FIRST=0
        export SAT_TRACE=0
        (/usr/bin/time -v timeout $timeout_secs $exec_bin $ltlf_file $part_file) &> $res_file
    elif [[ $exec_base == ltlfsyn_env* ]]; then
        # ltlfsyn env
        export TIME_LIMIT=$timeout_mins
        export WHICH_FIRST=0
        export SAT_TRACE=0
        (/usr/bin/time -v timeout $timeout_secs $exec_bin $ltlf_file $part_file) &> $res_file
    elif [[ $exec_base == cynthia* ]]; then
        # cynthia
        # default location /public/home/jwli/workSpace/yongkang/23.0802/cynthia-app
        (/usr/bin/time -v timeout $timeout_secs $exec_bin -n -f $ltlf_file --part $part_file) &> $res_file
    elif [[ $exec_base == lisa_env_syntcomp* ]]; then
        # === MUST BEFORE others === #
        # lisa_env_syntcomp
        # /public/home/jwli/workSpace/yongkang/JACM-24March-labs/bins/lisasyntcomp/lisa_env_syntcomp_default.sh
        cd /public/home/jwli/workSpace/yongkang/JACM-24March-labs/bins/lisasyntcomp
        (/usr/bin/time -v timeout $timeout_secs ./starexec_run_seqreal1.sh $tlsf_file) &> $res_file
    elif [[ $exec_base == lisa_env* ]]; then
        # lisa_env
        # /public/home/jwli/workSpace/yongkang/23.0906/lisa_env-static
        export PATH=$PATH:/public/home/jwli/workSpace/yongkang/usr/bin
        export LD_LIBRARY_PATH=$LD_LIBRARY_PATH:/public/home/jwli/workSpace/yongkang/usr/lib
        ( mkdir -p $PWD$ltlf_file ; cd $PWD$ltlf_file; time timeout $timeout_secs $exec_bin -syn -ltlf $ltlf_file -part $part_file) &> $res_file
    elif [[ $exec_base == lisa_sys* ]]; then
        # lisa
        # /public/home/jwli/workSpace/yongkang/23.0906/lisa_sys-static
        export PATH=$PATH:/public/home/jwli/workSpace/yongkang/usr/bin
        export LD_LIBRARY_PATH=$LD_LIBRARY_PATH:/public/home/jwli/workSpace/yongkang/usr/lib
        (/usr/bin/time -v timeout $timeout_secs $exec_bin -syn -ltlf $ltlf_file -part $part_file) &> $res_file
    elif [[ $exec_base == lydia_env_syntcomp* ]]; then
        # === MUST BEFORE others === #
        # lydia_env_syntcomp
        # /public/home/jwli/workSpace/yongkang/JACM-24March-labs/bins/lydia_env_syntcomp_static
        ( cd /public/home/jwli/workSpace/yongkang/JACM-24March-labs/bins/ ; time timeout $timeout_secs $exec_bin -f $tlsf_file) &> $res_file
    elif [[ $exec_base == lydia_env* ]]; then
        # lydia_env
        # /public/home/jwli/workSpace/yongkang/23.0803/lydia_env
        (/usr/bin/time -v timeout $timeout_secs $exec_bin --env -n -l ltlf -f $ltlf_file --part $part_file) &> $res_file
    elif [[ $exec_base == lydia_sys* ]]; then
        # lydia
        # /public/home/jwli/workSpace/yongkang/23.0803/lydia_sys
        (/usr/bin/time -v timeout $timeout_secs $exec_bin -n -l ltlf -f $ltlf_file --part $part_file) &> $res_file
    elif [[ $exec_base == nike_env* ]]; then
        # nike
        # /public/home/jwli/workSpace/yongkang/JACM-24March-labs/bins/nike
        (time timeout $timeout_secs $exec_bin --no-empty --file $ltlf_file --part $part_file -m bdd -s random) &> $res_file
    else
        echo "no matched exec_bin type" >&2
    fi
}
executeCase $1
